Formal Reasoning about Fine-Grained Access Control Policies

de Dios, M.A.G., Dania, C. and Clavel, M.

Nowadays, most of the main database management systems offer, in one way or another, the possibility of protecting data using _ne-grained access control (FGAC) policies, i.e., policies that depend on dynamic properties of the system state. Reasoning about FGAC policies typically amounts to answering questions about whether a security-related property holds in a (possibly infinite) set of system states. To carry out this reasoning, we propose a novel, tool-supported methodology, which consists in transforming the aforementioned questions about FGAC policies into satisfiability problems in first-order logic. In addition, we report on our experience using the Z3 Satisfiability Modulo Theory (SMT) solver for automatically checking the satisfiability of the first-order formulas generated by the tool implementing our methodology, called SecProver, for a non-trivial set of examples.

Cite as: de Dios, M.A.G., Dania, C. and Clavel, M. (2015). Formal Reasoning about Fine-Grained Access Control Policies. In Proc. 11th Asia-Pacific Conference on Conceptual Modelling (APCCM 2015) Sydney, Australia. CRPIT, 165. Saeki, M. and Kohler, H. Eds., ACS. 91-100

(from crpit.com) (local if available)